(declare-fun eax_in () (_ BitVec 32))
(declare-fun ecx_in () (_ BitVec 32))
(declare-fun ebx_in () (_ BitVec 32))
(declare-fun eax1 () (_ BitVec 32))
(declare-fun eax2 () (_ BitVec 32))
(declare-fun eax3 () (_ BitVec 32))
(declare-fun ecx1 () (_ BitVec 32))
(declare-fun ecx2 () (_ BitVec 32))
(assert (and (= eax1 (bvadd eax_in ebx_in)) (= eax2 (bvadd eax1 ecx_in)) (= ecx1 (bvand ecx_in #x000000ff)) (= eax3 (bvor eax2 ecx1))))
(assert (= eax3 #xffffffff))
(check-sat)
